$\forall$$E$, $X_{1}$, $X_{2}$:Type, ${\it pred?}$:($E$$\rightarrow$($E$+Unit)), ${\it info}$:($E$$\rightarrow$(Id$\times$$X_{1}$+(IdLnk$\times$$E$)$\times$$X_{2}$)), $r_{1}$, $r_{2}$, $x$:$E$.
\\[0ex]SWellFounded($\neg$first($y$) \& $x$ $=$ pred($y$)) $\Rightarrow$ $r_{2}$ before $r_{1}$ $\in$ eventlist(${\it pred?}$;$x$) $\Rightarrow$ $r_{2}$ $<$ $r_{1}$